Skip to content

Conversation

@jprotopopov-ut
Copy link
Collaborator

This feature is necessary for Linux kernel module analysis.

@jprotopopov-ut jprotopopov-ut requested a review from sim642 January 14, 2026 08:03
@sim642 sim642 added this to the 2.1.0 milestone Jan 14, 2026
@jprotopopov-ut
Copy link
Collaborator Author

I attempted to convert the example to get rid of _Static_assert's via the following trick:

#define ASSERT_TYPE3(_expr, _type, _c) \
    struct assertType##_c { \
        int x: _Generic(_expr, _type : 1, default : -1); \
    } assertValue##_c = {0}
#define ASSERT_TYPE2(_expr, _type, _c) ASSERT_TYPE3(_expr, _type, _c)
#define ASSERT_TYPE(_expr, _type) ASSERT_TYPE2(_expr, _type, __COUNTER__)

// ...
ASSERT_TYPE(&ptr, const int **);

but apparently CIL is fine with negative bit-field widths. Goblint is not, but the error it encounters is downstream from the actual issue:

Fatal error: exception Invalid_argument("Z.shift_left: count argument must be positive")

Furthermore, the following error probably warrants a separate ticket: Error: __auto_type unsupported for globals.

As for supposed difference between auto type inference and typeof, I believe it's rather straightforward. auto performs lvalue (and other) conversions, whereas typeof yields the type verbatim. Observed difference in behaviour wrt function parameters is explained by the fact that function parameters undergo respective conversions independently of typeof. The footnote in 6.7.3.6 refers to the section 6.9.2 ("Function definitions") which itself defers function parameter type adjustment to 6.7.7.4 ("Function declarators"). It is apparent that the intention of the footnote was just restating that these adjustments need to be respected by typeof.

@sim642 sim642 mentioned this pull request Jan 15, 2026
@sim642 sim642 changed the title Permit non-pure expressions in __auto_type Permit impure expressions in __auto_type Jan 15, 2026
@sim642 sim642 merged commit 7797529 into goblint:develop Jan 15, 2026
15 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants